$\forall$$L$:MsgA List. ma{-}is{-}empty($\oplus$($L$)) $\Leftrightarrow$ reduce($\lambda$$M$,$x$. ma{-}is{-}empty($M$) \& $x$;True;$L$)